WebAssembly 形式手法
WebAssembyは
Isabelle/HOL
で
well-defined
に定義されている
『Formal Methods and the WebAssembly Specification』
『Mechanising and Verifying the WebAssembly Specification』
Coqの方でやっているものもある
WasmCert/WasmCert-Coq: A mechanisation of Wasm in Coq
2018/04/29
WebAssembly - Archive of Formal Proofs
確認用
Q. WebAssembly 形式手法
参考
『Formal Methods and the WebAssembly Specification』
『Mechanising and Verifying the WebAssembly Specification』
関連
Isabelle